\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ \=($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $m$, ${\it m'}$:E.\+
\\[0ex]([$m$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [$m$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]$\Rightarrow$ ([${\it m'}$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [${\it m'}$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $\neg$f2f+{-}pred($e$,$m$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $\neg$f2f+{-}pred($e$,${\it m'}$))
\\[0ex]$\Rightarrow$ ($m$ = ${\it m'}$))
\-
\end{tabbing}